% -*- prolog -*-
%

%:- spy compile_type.

%:- uwrandomize(`div2).
%:- randomize(numeral).

p(X).
%p(X) :- fail.

plus(X,0,X).

plus(X,s(Y),Z) :- 
	plus(s(X),Y,Z).

minus(C,B,A) :- plus(A,B,C).

% numeral(_).
numeral(0).
numeral(s(X)) :- numeral(X).

lt(0,s(0)).
lt(0,s(Y)) :- lt(0,Y).
lt(s(X),s(Y)) :- lt(X,Y).

neg_lt(A,B) :- A = B.
neg_lt(A,B) :- lt(B,A).

gt(A,B) :- lt(B,A).

% t :- neg_mod(s(s(0)),s(0),s(0)).
t :- lt(0,s(0)).
%t :- lt(s(s(s(0))),s(s(s(s(0))))).

% Assumes C is ground

neg_mod(X,0,Y). % needed to make mod a total function
                % rp does not yet have voids ...

neg_mod(A,B,C) :-
	neg_mod1(A,B,C).

neg_mod1(A,B,C) :- 
	lt(A,B),
	A \= C.

neg_mod1(A,B,C) :- 
	neg_lt(A,B),
	B \= 0,  % avoid division by zero errors
	minus(A,B,D),
	neg_mod1(D,B,C).

% If both A and B are non-ground ...
%neg_mod2(A,B,C) :-
%	gt(B,C),
%	lt(A,B),
%	A \== C.

%rnot `ndiv2(0).

%`div2(s(s(0))).

`div2(s(s(s(s(0))))).

%`div2(s(s(s(s(s(s(0))))))).

`div2(s(s(s(s(s(s(s(s(0))))))))).

%`div2(s(s(s(s(s(s(s(s(s(s(0))))))))))).

`div2(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))).

% :- print('try:\n exists - X ::: ( numeral(X), forall - Y ::: `div2(Y) => rnot n  ).\n').






